$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$, ${\it e'}$:E.
\\[0ex]@loc(${\it e'}$)($x$:$T$)
\\[0ex]$\Rightarrow$ ($e$ $<$loc ${\it e'}$)
\\[0ex]$\Rightarrow$ ((($x$ after $e$) = ($x$ when ${\it e'}$) $\in$ $T$) $\vee$ (($x$ after lastchange($x$;${\it e'}$)) = ($x$ when ${\it e'}$) $\in$ $T$))